Nuprl Lemma : subtype-fpf
0,22
postcript
pdf
A
:Type,
P
:(
A
Prop),
B
:(
A
Type).
a
:{
a
:
A
|
P
(
a
) } fp
B
(
a
)
a
:
A
fp
B
(
a
)
latex
Definitions
x
:
A
.
B
(
x
)
,
A
&
B
,
True
,
T
,
P
Q
,
{
T
}
,
P
Q
,
P
&
Q
,
False
,
,
A
B
,
||
as
||
,
l
[
i
]
,
P
Q
,
(
x
l
)
,
x
(
s
)
,
a
:
A
fp
B
(
a
)
,
Prop
,
S
T
,
S
T
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
l
member
wf
,
nil
member
,
cons
member
,
select
wf
,
length
wf1
origin
A:Type, P:(A
Prop), B:(AType). a:{a:A| P(a) } fp B(a) 
a:A fp B(a) A:Type, P:(AProp), B:(AType). a:{a:A| P(a) } fp B(a) a:A fp B(a) 
x:A. B(x)
T
Q
Q
B
Q
l) B(a)
T Tx:A. B(x) T